Inference at * 1 1 
Iof proof for Lemma absval elim:



1. P : 
2. x : 
3. P(|x|)
  P(x) 

latex

 by ((MoveToConcl 3) 
CollapseTHEN (Unfold `absval` 0)) 

latex

C1: 

C1: 2. x : 
C1:   (P(if 0 z x then x else -x fi ))  (P(x))
C.

Definitions

|i|, P  Q